/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import alloy.ast.BinaryExpr;
import alloy.ast.Expr;
import alloy.ast.HasType;
import alloy.ast.Invocation;
import alloy.ast.Node;
import alloy.type.UnionType;

/**
 * This class formats type error messages and prints them to the Dbg.user 
 * buffer.  It also keeps track of whether any error messages have been
 * printed out or not.
 **/
public class TypeErrorReporter extends ErrorReporter {

    public TypeErrorReporter() {super();}
    
    public TypeErrorReporter(boolean report_) {super(report_);}
    
    /**
     * @param nodeDesc description of the node (e.g. "Left" or "Right" to describe
     * the left or right child of a binary expression)
     * @param node a typed expression 
     * @return a String of the form 
     * "<nodeDesc>: <node.nodeString()> has type <node.getType()>" if node's type has been set
     * "<nodeDesc>: <node.nodeString()>" otherwise
     **/
    public static String format(String nodeDesc, HasType node) {
	UnionType type = node.getType();
	return (nodeDesc + ": " + node.nodeString() + 
		(type==null ? "" : " has type " + type.toString()));
    }

    /**
     * @param nodeDesc description of the node (e.g. "Formula" to describe
     * an elementary formula)
     * @param node an AST node
     * @return a String of the form 
     * "<nodeDesc>: <node.nodeString()>"
     **/
    public static String format(String nodeDesc, Node node) {
	return (nodeDesc + ": " + node.nodeString());
    }

    /**
     * @param expr expression
     * @return a String of the form 
     * "expression: <expr.nodeString()> has type <expr.getType()>" if node's type has been set
     * "expression: <expr.nodeString()>" otherwise
     **/
    public static String format(Expr expr) {
	return format("Expression", expr);
    }

    /**
     * @param errMsg the error message
     * @param binExpr the binary expression that contains the error
     * Reports a type error in a binary expression.  The message format is:
     * "Type Error: <errMsg>\n
     *  expression: <binExpr.nodeString()> [has type <type of binExpr>]\n
     *  left: <left child of binExpr> has type <left type>\n
     *  right: <right child of binExpr> has type <right type>"
     * Note:  the types of binExpr is reported if it has been assigned 
     * (that is, if its getType() method returns a UnionType).  We assume
     * that the types have been assigned to left and right children of binExpr
     **/
    public void type(String errMsg, BinaryExpr binExpr) {
	error("Type error: " + errMsg + "\n" +
	      format((Expr) binExpr) + 
	      format("\nLeft", (HasType) binExpr.getLeft()) + 
	      format("\nRight", (HasType) binExpr.getRight()),
	      (Node) binExpr);
	       
    }

    
    /**
     * @param errMsg the error message
     * @param node the node that contains the error
     * Reports a type error in a node.  The message format is:
     * "Type Error: <errMsg>"
     **/
    public void type(String errMsg, Node node) {
	error("Type error: " + errMsg, node);
    }

    /**
     * @param errMsg the error message
     * @param invocation invocation that contains the error
     * Reports an type error in a binary expression.  The message format is:
     * "Invocation Error: <errMsg>\n
     *  invocation: <invocation.nodeString()>"
     **/
    public void invocation(String errMsg, Invocation invocation) {
	error("Invocation error: " + errMsg + "\nInvocation: " + 
	      invocation.nodeString(), (Node) invocation);
    }

    /**
     * @param errMsg the error message
     * @param node the node that contains the error
     * Reports a type error in a node.  The message format is:
     * "Type Error: <errMsg>"
     **/
    public void invocation(String errMsg, Node node) {
	error("Invocation error: " + errMsg, node);
    }

}
